COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\\M0BDR25\M1BDI25\M2NGR40\M3XMAS25\.
C00007 ENDMK
C⊗;
\\M0BDR25;\M1BDI25;\M2NGR40;\M3XMAS25;\.
\F0\CCOMPUTER SCIENCE 256b
\CMATHEMATICAL THEORY OF COMPUTATION
\CSPRING 1973


\J	1. The \F1mathematical theory of computation\F0 is concerned with
proving assertions about particular computer programs.  This should be 
contrasted with the \F1theory of computability\F0 which is concerned with
determining what problems can be solved by whole classes of computer
programs.

	2. The original motivation for mathematical theory of computation
is technological.  Namely, its goal is to be able to prove formally that
computer programs meet their specifications and to check these proofs
by computer.  Then debugging the program can be replaced by debugging
the proof that the program is correct making such changes as may be
required in the program and proof of its correctness as will make the
proof checker agree that the specifications are met.  Once this is done
the assertions are correct if the proof checker and the system of logic
it embodies are correct.  The only remaining problem is whether the
assertions proved express the properties the program really ought to have.
We claim that this can increase the certainty that programs are correct
in a practical way.

	Besides this, since a program is a mathematical object and its
properties are logically determined by its form, it is a mathematical
disgrace that they are debugged rather than proved correct.

	In the various efforts to develop mathematical theory of computation
(MTC), many problems that have mathematical interest apart from the
potential interest have developed.  However, this course will concentrate
on the aspects of the matter that the instructor thinks have a reasonable
chance of contributing to the above mentioned goal.

	3. The first part of the course will be descriptive.  Two formalisms
for descibing procedures, the algolic program, and the recursive conditional
expression will be described.  The method of abstract syntax and its
application for defining programming languages will be presented.

	4. Next we have some relatively easy material concerning conditional
expressions, their transformations and their abstract syntax.  In connection
with this we shall introduce the use of Richard Weyhrauch's proof checker
for first order logic.

	5. Then we come to the methods of Floyd, Manna and Hoare for defining
and proving the correctness of algolic programs.

	6. Then the methods of recursion induction and Manna and Pnueli
for proving the correctness of recursively defined functions.

	7. Then the correctness of compilers.  Work of Burstall and McCarthy
and Painter will be discussed here.

	8. Finally, we shall discuss Scott's formalism for MTC involving
monotonic and continuous functions on lattices.

	There will be exercises and a midterm examination.

	A term project to be defined around midterm and involving a computer
checked proof of the correctness of a moderately substantial program is more
likely than a final examination.